Section: New Results

A new version of PlusCal

Participants : Sabina Akhtar, Stephan Merz, Martin Quinson [of project team AlGorille] .

In cooperation with Martin Quinson of the AlGorille team of INRIA Nancy we have defined and implemented a high-level language for the description of concurrent and distributed algorithms. Our work is inspired by Lamport's PlusCal [29] , but extends it for the modeling and verification of distributed algorithms. In particular, processes can be nested and variables are properly scoped; this is useful for modeling concurrent execution at different levels of a hierarchy (such as threads versus processes).

In 2011, the main effort has gone into designing partial-order reduction techniques for model checking PlusCal algorithms, which exploit the locality information present in the models. In particular, we have defined predicates that ensure the independence of two (blocks of) statements and adapted the TLC model checker to implement static partial-order reduction. Sabina Akhtar prepares her PhD thesis manuscript, and the thesis defense is planned for spring 2012.